package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{Formula,Imply}

import scala.util.parsing.input.Positional

  
sealed abstract class VTree extends Positional


final case class VProgram(constraint: Option[Formula], 
                          containers: List[VContainer])
                 extends VTree
                            

final case class VContainer(invariant: Option[Formula], 
                            methods: List[VMethodDef])
                 extends VTree
 

final case class VMethodDef(bindings: Formula, 
                            ppc: Option[(Formula,Formula)], 
                            body: VExpr) 
                 extends VTree


sealed abstract class VExpr extends VTree


final case class VIf(cond: (Formula,Formula), then: VExpr, elze: VExpr) 
                 extends VExpr

final case object VSimpleExpr extends VExpr


trait VPMatching
final case class VMatch(scrutinee: Formula, 
                        cases: List[VCaseDef]) 
                 extends VExpr 
                 with VPMatching

final case class VCaseDef(position: Int,
                          formula: Imply, 
                          body: VExpr) 
                 extends VPMatching
